Iof proof for Lemma tidentity wf:
A:Type. Id{A} 
A
A
by ((Unfold `tidentity` 0)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat
C3:n)) (first_tok :t) inil_term)))
C.| 12,41 |
A:Type. Id{A} AA
by ((Unfold `tidentity` 0)
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat
C3:n)) (first_tok :t) inil_term)))
C.
| Definitions | Tx:A. B(x) |
| Lemmas |